
module Hw1 : Hw1 =
struct

let t1 = `:bool`
let t2 = `:nat`
let t3 = `:real`
let t4 = `:int`
let t5 = `:nat#nat`
let t6 = `:nat->real`
let t7 = `:real->bool`
let t8 = `:nat->bool`
let t9 = `:(nat->bool)->bool`
let t10 = `:(real->bool)->bool`

let p1 = `T`
let p2 = `F`
let p3 = `P ==> Q`
let p4 = `P <=> Q`
let p5 = `~P`
let p6 = `~P ==> Q`
let p7 = `F ==> P`
let p8 = `P ==> F`
let p9 = `(T ==> P) <=> P`
let p10 = `(P ==> Q) <=> (~Q ==> ~P)`
let p11 = `!x. x * x >= &0`
let p12 = `!y. ?m. y < m`
let p13 = `?x. X x`
let p14 = `?X. !x. ~(X x)`
let p15 = `f x > g y`
let p16 = `x = y ==> f x = g y`
let p17 = `&0 < &1 / &2 /\ &1 / &2 < &1`
let p18 = `!x y. ~(x = y) ==> ~(f x = f y)`
let p19 = `!x. ?y. f y = x`
let p20 = `!e. e > &0 ==> ?d. abs(x - y) < e ==> abs (f x - f y) < d`
let p21 = `A SUBSET B`
let p22 = `A INTER B = C`
let p23 = `A UNION B = C`
let p24 = `A INTER B = B INTER A`
let p25 = `A UNION B SUBSET C`
let p26 = `?n. &2 pow n > &17`
let p27 = `?n. &2 pow n > &777 / &1000`
let p28 = `(&3:int) - &4 = -- &1`
let p29 = `&3 - &4 = -- &1`
let p30 = `--(-- &4) + &3 - &7`
let p31 = `&3 + (-- &4)`
let p32 = `&1 / &0`
let p33 = `UNIONS X = C`
let p34 = `{}`
let p35 = `{}`
let p36 = `(1, 2)`
let p37 = `{1, 2, 3}`
let p38 = `CARD {1, 2, 3} = 3`

let h1 = `X:A`
let h2 = `x:real`
let h3 = `X:real->bool`
let h4 = `X = (UNIV:real->bool)`
let h5 = `v:real^3`
let h6 = `(v:real^3) + w`
let h7 = `X : (real->bool)->bool`
let h8 = `-- (v:real^3)`
let h9 = `(v:real^3) $ 3`
let h10 = `&3 % (v:real^3)`
let h11 = `(v:real^3) dot w`
let h12 = `&2 % (v:real^3) + &4 % w - &7 % u`

end

